<!doctype html>
<html lang="en">
  <head>
    <!-- Required meta tags -->
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">

    <!-- Bootstrap CSS -->
	<!--<link rel="stylesheet" href="css/bootstrap.min.css" >-->
	<link rel="stylesheet" href="https://leanprover-community.github.io//css/lean.css" >
	<link rel="stylesheet"
          href="https://fonts.googleapis.com/css?family=Merriweather:700">
    

	<script>
                function buildShortcutsForStructures(names) { 
                        const o = {}
                        names.forEach(name => o[name] = `\\mathbb\{${name}\}`)
                        return o
                }
		MathJax = {
			  tex: {
                                  macros: {
                                          ...buildShortcutsForStructures(["R", "Q", "Z", "N", "C"]),
                                  },
				      inlineMath: [['$', '$'], ['\\(', '\\)']]
				    },
		};
	</script>
	<script type="text/javascript" id="MathJax-script" async
		  src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-chtml.js">
	</script>

	<title>Using leanproject</title>
  </head>
  <body>
  <div id="wrapper">
  <nav class="navbar navbar-expand-lg navbar-light bg-gradient-light">
    <div class="d-flex flex-grow-1">
		<a class="navbar-brand" href="https://leanprover-community.github.io/index.html">Lean Community
    </a>
    </div>

    <button class="navbar-toggler" type="button" data-toggle="collapse" data-target="#navbarSupportedContent" aria-controls="navbarSupportedContent" aria-expanded="false" aria-label="Toggle navigation">
      <span class="navbar-toggler-icon"></span>
    </button>
    <div class="collapse navbar-collapse flex-grow-1 text-right" id="navbarSupportedContent">
      <ul class="navbar-nav ml-auto">
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Try it!
          </a>
		  <div class="dropdown-menu " aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/lean-web-editor">Lean online</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/get_started.html">Install</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Learn
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/learn.html">Resources</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.github.io/theorem_proving_in_lean/">Theorem proving in Lean</a>
			
			
			
			<a class="dropdown-item" href="http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/">The natural number game</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib-overview.html">Library overview</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib_docs">API documentation</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Community
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html">Meet us</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.zulipchat.com/">Zulip chat</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html#maintainers">Maintainers</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/contribute/index.html">How to contribute</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/papers.html">Papers</a>
			
			
          </div>
        </li>
		
      </ul>
    </div>
  </nav>
  <div class="container-sm mt-4">
	  
<h1 id="using-leanproject" class="markdown-heading">Using leanproject <a class="hover-link" href="#using-leanproject">#</a></h1>
<h2 id="basic-usage" class="markdown-heading">Basic usage <a class="hover-link" href="#basic-usage">#</a></h2>
<p>Everything is done using the <code>leanproject</code> command-line tool. You can
use <code>leanproject --help</code> to get the list of available commands and
options.</p>
<h3 id="getting-an-existing-lean-project" class="markdown-heading">Getting an existing Lean project <a class="hover-link" href="#getting-an-existing-lean-project">#</a></h3>
<p>The command to fetch an existing project from GitHub and make sure it
includes a copy of mathlib ready to go is <code>leanproject get name</code> where
name is either a git url, such as <code>https://github.com/leanprover-community/tutorials.git</code>
or <code>git@github.com:leanprover-community/tutorials.git</code>, or a GitHub project
identifier such as <code>leanprover-community/tutorials</code>. The organization
name defaults to <code>leanprover-community</code> so the simplest way get the tutorials
project is to run:</p>
<pre><code>leanproject get tutorials
</code></pre>
<p>You can specify a git branch name <code>my_branch</code> by appending
<code>:my_branch</code> at the end of the specified name (without space).
By default this branch should be an existing branch.
Use <code>leanproject get -b project_name:branch_name</code> to get
the project <code>project_name</code> and then create a branch <code>branch_name</code>
and start working on it.
You can also specify a target directory name as a second argument to the
command.</p>
<h3 id="creating-a-new-project" class="markdown-heading">Creating a new project <a class="hover-link" href="#creating-a-new-project">#</a></h3>
<p>You can create a project in a new folder <code>my_project</code> by running:</p>
<pre><code>leanproject new my_project
</code></pre>
<p>If you omit the argument, the project will be created directly inside
the current folder. This new project will be using the latest version of
Lean compatible with mathlib, and include a pre-built mathlib.</p>
<h3 id="building-a-project" class="markdown-heading">Building a project <a class="hover-link" href="#building-a-project">#</a></h3>
<p>Only mathlib itself comes with pre-built olean files. In order to build
oleans in a project (which is needed for every non-trivial project in
order to get decent interactive Lean speed), you can use:</p>
<pre><code>leanproject build
</code></pre>
<h3 id="getting-mathlib-oleans" class="markdown-heading">Getting mathlib oleans <a class="hover-link" href="#getting-mathlib-oleans">#</a></h3>
<p>In an existing project depending on mathlib (or in mathlib itself), you
can run:</p>
<pre><code>leanproject get-mathlib-cache
</code></pre>
<p>to download a compiled mathlib at the commit currently specified in the
project <code>leanpkg.toml</code> (see the next section if you want to update this
commit and get the latest mathlib).</p>
<h3 id="upgrading-mathlib" class="markdown-heading">Upgrading mathlib <a class="hover-link" href="#upgrading-mathlib">#</a></h3>
<p>In an existing project depending on mathlib, you can upgrade to the
latest mathlib version by running:</p>
<pre><code>leanproject upgrade-mathlib
</code></pre>
<p>This can be abbreviated to <code>leanproject up</code>.
By default, this will update the version of Lean used by this project to
match the latest version compatible with mathlib. You can forbid such an
upgrade by using <code>leanproject --no-lean-upgrade upgrade-mathlib</code>.</p>
<h2 id="advanced-usage" class="markdown-heading">Advanced usage <a class="hover-link" href="#advanced-usage">#</a></h2>
<h3 id="global-mathlib-install" class="markdown-heading">Global mathlib install <a class="hover-link" href="#global-mathlib-install">#</a></h3>
<p>If you want to use mathlib outside of a Lean project, you can run:</p>
<pre><code>leanproject global-install
</code></pre>
<p>This will put a pre-compiled mathlib inside <code>$HOME/.lean</code>, the user-wide
Lean project whose dependencies can be used by lean files outside
projects. You can upgrade this project using:</p>
<pre><code>leanproject global-upgrade
</code></pre>
<h3 id="adding-mathlib-to-an-existing-project" class="markdown-heading">Adding mathlib to an existing project <a class="hover-link" href="#adding-mathlib-to-an-existing-project">#</a></h3>
<p>If you already have a Lean project but it doesn't use mathlib yet, you
can go to the project folder and run:</p>
<pre><code>leanproject add-mathlib
</code></pre>
<p>By default, this will update the version of Lean used by this project to
match the latest version compatible with mathlib. You can forbid such an
upgrade by using <code>leanproject --no-lean-upgrade add-mathlib</code>.</p>
<h3 id="project-olean-cache" class="markdown-heading">Project olean cache <a class="hover-link" href="#project-olean-cache">#</a></h3>
<p>In any Lean project, it can be useful to store and retrieve olean files,
especially if the project has several git branches. Storing oleans is
done by:</p>
<pre><code>leanproject mk-cache
</code></pre>
<p>while retrieving them is done by:</p>
<pre><code>leanproject get-cache
</code></pre>
<p>One should note that, although olean files are indeed the primary target
here, these commands actually store everything from the
<code>src</code> and <code>test</code> folders of the current project.</p>
<p>If the project is mathlib itself, the caches will be stored in
<code>$HOME/.mathlib/</code>. Otherwise, they will be stored in a folder <code>_cache</code> inside
the project top-level folder. They are named after the corresponding git
commit hash.</p>
<p>In general, using these commands in a dirty git repository (<em>ie</em> a
repository whose working copy contains uncommitted changes) is a bad
idea. You can do it anyway by running <code>leanproject mk-cache --force</code> or
<code>leanproject get-cache --force</code> respectively.</p>
<p>The <code>--force</code> option will also overwrite existing cache for the current
git revision.</p>
<p>When using <code>get-cache</code> inside the mathlib project, the local cache in
<code>$HOME/.mathlib/</code> will be searched first, before trying to download it.
You can force download by running
<code>leanproject --force-download get-cache</code>. This <code>--force-download</code> option
can also be used with the <code>upgrade-mathlib</code> command.</p>
<h3 id="import-graphs" class="markdown-heading">Import graphs <a class="hover-link" href="#import-graphs">#</a></h3>
<p>If you want to generate a graph file showing your project import
structure, you can run:</p>
<pre><code>leanproject import-graph my_graph_file_name.suffix
</code></pre>
<p>where the suffix will determine the output format. It must be either
<code>dot</code> or <code>graphml</code> or <code>gexf</code>, (or <code>pdf</code>, <code>svg</code> or <code>png</code> if
<a href="https://www.graphviz.org/">graphviz</a> is installed).
If you want to restrict the graph to files leading to a certain file
<code>my_subproject/my_file.lean</code> then you can run:</p>
<pre><code>leanproject import-graph --to my_subproject.my_file my_graph_file_name.suffix
</code></pre>
<p>Dually, if you want to see all files using <code>my_subproject/my_file.lean</code>
then you can run:</p>
<pre><code>leanproject import-graph --from my_subproject.my_file my_graph_file_name.suffix
</code></pre>
<p>Combining <code>--to</code> and <code>--from</code> is possible.</p>
<h3 id="git-hooks" class="markdown-heading">Git hooks <a class="hover-link" href="#git-hooks">#</a></h3>
<p>If you want leanproject to fetch olean caches after each <code>git checkout</code>,
and make olean caches after each <code>git commmit</code> in the current project,
you can run:</p>
<pre><code>leanproject hooks
</code></pre>
<p>Beware this will overwrite any <code>post-checkout</code> or <code>post-commit</code> file you
might have in your project <code>.git/hooks</code>.</p>
<h3 id="cache-download-url-handling" class="markdown-heading">Cache download url handling <a class="hover-link" href="#cache-download-url-handling">#</a></h3>
<p>By default, leanproject will try to find mathlib olean files hosted on an
Azure server. You permanently override the base url it uses by running:</p>
<pre><code>leanproject set-url my_url
</code></pre>
<p>so that leanproject will look for caches at
<code>my_url/relevant_git_hash.tar.gz</code>. You can override this base url
for one invocation using <code>leanprover --from-url my_url ...</code>
(where <code>...</code> denotes a command and its arguments).</p>
<h2 id="troubleshooting" class="markdown-heading">Troubleshooting <a class="hover-link" href="#troubleshooting">#</a></h2>
<p>If <code>leanproject</code> ends with a mysterious error message, you can run it
using the <code>--debug</code> flag, e.g. <code>leanproject --debug new my_project</code>.
It will then probably output a python trace that you'll be able to paste
in a GitHub issue or on <a href="https://leanprover.zulipchat.com/">Zulip</a>.</p>

  </div>
</div>

  <nav class="footer navbar navbar-expand-lg navbar-light bg-light justify-content-end">
  <ul class="nav">
    <li class="nav-item">
      <a class="nav-link active" href="https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/templates/leanproject.md">Suggest edits to this page on GitHub</a>
    </li>
  </ul>
</nav>

    <script src="https://code.jquery.com/jquery-3.4.1.slim.min.js" integrity="sha384-J6qa4849blE2+poT4WnyKhv5vZF5SrPo0iEjwBvKU7imGFAV0wwj1yYfoRSJoZ+n" crossorigin="anonymous"></script>
    <script src="https://leanprover-community.github.io//js/bootstrap.min.js"></script>
    
  </body>
</html>